COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Some notes for the book
C00004 ENDMK
C⊗;
Some notes for the book

Perhaps there should be an internal form of sentences, i.e.
(ALL (X Y) etc.
This would permit exercises about proof-finding and checking -
perhaps even microBoyer.

An exercise about recognizing a large class of LISP programs guaranteed to
terminate could be included.  An elaborate version of this could be a term
project.

There needs to be an explanation of common lisp terminology
including various solecisms, especially Winston's use of "function".

It looks increasingly as though all inductions should be based on
rank, and that the list and S-expression induction schemata are not
worthwhile.  Malik's 1980 paper seems to show this.

Lift various ideas from Winston's book.  Noted in my copy.